Compositional Reasoning for Shared-variable Concurrent Programs

摘要

Scalable and automatic formal verification for concurrent systems is alwaysdemanding, but yet to be developed. In this paper, we propose a verificationframework to support automated compositional reasoning for concurrent programswith shared variables. Our framework models concurrent programs as succinctautomata and supports the verification of multiple important properties. Safetyverification and simulations of succinct automata are parallel compositional,and safety properties of succinct automata are preserved under refinements.Formal verification of finite state succinct automata can be automated.Furthermore, we propose the first automated approach to checking rely-guaranteebased simulations between infinite state concurrent programs. We haveprototyped our algorithm and applied our tool to the verification of multiplerefinements.